Functional programming.md (3125B)
1 +++ 2 title = 'Functional programming' 3 +++ 4 # Functional programming 5 ## Inductive types 6 Mottoes: 7 - no junk: type contains no values except those expressible using constructors 8 - e.g. for `nat`, there aren't values that can't be expressed using finite combination of `zero` and `succ` 9 - no confusion: values built in different ways are different 10 - e.g. for `nat`, `zero` ≠ `succ x` 11 12 ## Structural induction 13 generalization of math induction to inductive types. 14 - to prove property `P[n]` for natural numbers `n`, prove: 15 - base case `P[0]` 16 - induction step `∀k, P[k] → P[k+1]` 17 - similarly for lists: 18 - base case `P[[]]` 19 - induction step `∀y ys, P[ys] → P[y :: ys]` 20 21 Example proof: 22 23 ```lean 24 lemma nat.succ_neq_self (n : Ν) : 25 nat.succ n ≠ n := 26 begin 27 induction' n, 28 { simp }, 29 { simp [ih] } 30 end 31 ``` 32 33 You can use `case` to supply custom names and/or reorder cases. 34 35 ## Structural recursion 36 Form of recursion where you can peel off constructors from value. 37 Hence only call themselves finitely many times. 38 39 Example: 40 41 ```lean 42 def fact : Ν → Ν 43 | 0 := 1 44 | (n+1) := (n+1) * fact n 45 ``` 46 47 ## Pattern matching 48 `match` lets you do nonrecursive pattern matching 49 50 ``` 51 match term_1, term_2, ..., term_n with 52 | pattern_1, ..., pattern_m := result_1 53 ... 54 | pattern_k1, ..., pattern_km := result_k 55 end 56 ``` 57 58 ## Structures 59 You can define records/structures, essentially nonrecursive single-constructor inductive types. 60 61 ```lean 62 structure rgb := (red green blue : Ν) 63 def red : rgb := 64 { red := 0xff, 65 green := 0x00, 66 blue := 0x00 } 67 68 structure rgba extends rgb := (alpha : Ν) 69 def semitransparent_red : rgba := 70 { alpha := 0x7f, 71 ..pure_red } 72 ``` 73 74 `cases` does a case distinction on a term, giving rise to as many subgoals as constructors in definition of term's type. 75 76 77 ## Type classes 78 Structure type combining abstract constants and their properties. 79 Type can be declared instance of type class by (1) providing concrete definitions for constants and (2) proving that properties hold. 80 81 for example, for class: 82 83 ```lean 84 class inhabited (α : Sort u) := (default [] : α) 85 ``` 86 87 you can declare an instance like this: 88 89 ```lean 90 @[instance] def nat.inhabited : inhabited Ν := { default := 0 } 91 92 @[instance] def list.inhabited : {α : Type} : inhabited (list α) := { default := [] } 93 ``` 94 95 ## Lists 96 Inductive polymorphic types constructed from `nil` and `cons`. 97 98 `cases'` can be used on hypothesis of form `l = r`. Matches `r` against `l`, replaces all occurrences of vars in `r` with corresponding terms in `l` globally across goal. 99 it can also do case distinction on proposition, yielding one subgoal where the prop is true, and one where it's false. 100 101 `list.map` applies function element-wise to list. 102 `list.tail` gets everything but first element. 103 `list.head` gets first element. 104 `list.zip` takes two lists, and creates list of pairs. 105 `list.length` returns number of elements. 106 107 ## Binary trees 108 Inductive types with constructors taking recursive arguments. 109 Have nodes with max two children. 110 111 ```lean 112 inductive btree (α : Type) : Type 113 | empty {} : btree 114 | node : α → btree → btree → btree 115 ```